$\forall$${\it da}$:fpf(Knd; $k$.Type), $k$:Knd. normal{-}da\{i:l\}(${\it da}$) $\Rightarrow$ normal{-}type\{i:l\}(ma{-}valtype(${\it da}$; $k$))